i:Id, l:IdLnk, da:fpf(Knd; k.Type), tg:Id, k:Knd, n,f:top.
msg-spec-loc-decl(msg-spec1(k; l; tg; n; s,v.f(s,v)); i; da)
 ((source(l) = i)  (fpf-dom(Kind-deq; rcv(l,tg); da))) 

latex

Definitions

t  T, P  Q, x:A. B(x), b, P  Q, <a, b>, Knd, Type, x.A(x), x. t(x), fpf(A; a.B(a)), top, x:AB(x), rcv(l,tg), Kind-deq, fpf-dom(eq; x; f), prop{i:l}, source(l), Id, s = t, x:A  B(x), IdLnk, P  Q, P  Q, type List, [], cons(car; cdr), (x  l), guard(T), void, isect(A; x.B(x)), idlnk-deq, product-deq(A; B; a; b), fpf-single(x; v), l_all(L; T; x.P(x)), msg-spec-loc-decl(snd; i; da), msg-spec1(k; l; tg; n; s,v.f(s;v)), left + right, P  Q, decidable(P), False, A, sq_type(T), sqequal(s; t), atom{$n:n}, t.2, t.1, True, tt,

Lemmas

bool sq, assert elim, decidable assert, IdLnk sq, pi1 wf, pi2 wf, Id sq, decidable equal Id, fpf wf, fpf-single-dom, fpf-single wf, top wf, product-deq wf, idlnk-deq wf, iff functionality wrt iff, and functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, l member wf, IdLnk wf, Id wf, lsrc wf, assert wf, fpf-dom wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf